module SWIMv2

// Boolean data type
abstract sig Bool {}
one sig True extends Bool { }
one sig False extends Bool { }

// Concepts being used as signature properties
sig Email {}
sig Password {}
sig Name {}
sig Image {}
sig Text {}

// A skill only has a name, but it is not a string by itself
sig Skill {
	name: one Name,
	description: one Text,
	proposer: one User,
	approver: lone Administrator
}

one sig SkillDatabase {
	skills : set Skill
}

fact {
	// No two skills can have the same name
	no skill1, skill2 : Skill | skill1 != skill2 and skill1.name = skill2.name

	// If two skill have different name then they need to have different description
	all skill1, skill2: Skill | skill1.name != skill2.name implies skill1.description != skill2.description
}

// An external visitor. We know no information about him
sig Visitor {}

// Registered user
sig User {
	// Profile
	email: one Email,
	username: one Name,
	password: one Password,
	avatar: lone Image,
	info: lone String,
	// Skills
	skills: set Skill,
	// Social
	friends: set User,
	// Permissions
	demoted: one Bool
}

// Administrator
sig Administrator extends User {}

// Super user
sig SuperUser extends Administrator { }

fact {
	// The same email cannot be used by more than 1 user
	no user1, user2 : User | user1 != user2 and user1.email = user2.email

	// An user cannot be friend with himself
	all user : User | !(user in user.friends)

	// The friendship relation is symmetric
	all user1, user2 : User | (user1 in user2.friends) => (user2 in user1.friends)

	// There not exist demoted administrators or super users 
	no admin : Administrator | admin.demoted in True

	// Users' skills must be within the database
	all user : User | one db : SkillDatabase | all skill : Skill |
		skill in user.skills => skill in db.skills
}

// Messages. For simplicity, we assume a message is sent only to one user
sig Message {
	sender: one User,
	recipient: one User,
	content: one Text
}

fact {
	// Users cannot send messages to themselves
	no message : Message | message.sender = message.recipient
}

abstract sig Rating {}
one sig OneStar, TwoStars, ThreeStars, FourStars, FiveStars extends Rating {}

// Feedback records
sig Feedback {
	author: one User,
	target: one User,
	rating: one Rating,
	skill: one Skill,
	comment: one Text
}

fact {
	// Users cannot provide feedback for themselves
	all feedback : Feedback | feedback.author != feedback.target

	// A feedback should be about a skill that the target owns
	all feedback : Feedback | feedback.skill in feedback.target.skills

	// There cannot exist more than 1 feedback on the same user about the same skill from the same author
	no feed1, feed2 : Feedback |
		feed1 != feed2 and 
		feed1.author = feed2.author and
		feed1.target = feed2.target and
		feed1.skill = feed2.skill

	// All skills in feedback must be approved
	all feedback: Feedback | #(feedback.skill.approver) = 1
}

// ---- DYNAMICS samples ----
// Skills edit

pred addSkill[user, result : User, skill : Skill] {
	// Preconditions
	skill !in user.skills and #(skill.approver) = 1
	// Postconditions
	result.email = user.email
	result.username = user.username
	result.password = user.password
	result.avatar = user.avatar
	result.info = user.info
	result.friends = user.friends
	result.demoted = user.demoted

	result.skills = user.skills + skill
}

pred delSkill[user, result : User, skill : Skill] {
	skill in user.skills and #(skill.approver) = 1

	result.email = user.email
	result.username = user.username
	result.password = user.password
	result.avatar = user.avatar
	result.info = user.info
	result.friends = user.friends
	result.demoted = user.demoted

	result.skills = user.skills - skill
}

assert skillSetAdditionIntegrity {
	all user, temp : User, skill : Skill | 
		addSkill[user, temp, skill] => 
		#(temp.skills) > #(user.skills) and skill in temp.skills
}

assert skillSetDeletionIntegrity {
	all user, temp : User, skill : Skill | 
		delSkill[user, temp, skill] => 
		#(temp.skills) < #(user.skills) and !(skill in temp.skills)
}

assert skillSetIdempotency {
	all user, temp1, temp2 : User, skill : Skill | 
		addSkill[user, temp1, skill] and delSkill[temp1, temp2, skill] => 
		user.skills = temp2.skills
}

check skillSetAdditionIntegrity for 3
check skillSetDeletionIntegrity for 3
check skillSetIdempotency for 3


// Skills proposals

pred proposeSkill[db, db' : SkillDatabase, user : User, skill : Skill] {
	// Preconditions
	skill.proposer = user and (skill.approver & User) = none and skill !in db.skills
	// Postconditions
	db'.skills = db.skills + skill
}

pred approveSkill[db, db' : SkillDatabase, admin : Administrator, skill, skill' : Skill] {
	skill in db.skills and #(skill.approver) = 0

	skill'.name = skill.name
	skill'.description = skill.description
	skill'.proposer = skill.proposer

	skill'.approver = admin
	db'.skills = (db.skills - skill) + skill'
}

assert skillProposal {
	all db, db' : SkillDatabase, user : User, skill : Skill |
		proposeSkill[db, db', user, skill] =>
		#(db'.skills) > #(db.skills) and skill in db.skills
}

assert skillApproval {
	all db, db' : SkillDatabase, admin : Administrator, skill, skill' : Skill |
		approveSkill[db, db', admin, skill, skill'] =>
		skill' in db.skills and skill'.approver = admin
}

check skillProposal for 3
check skillApproval for 3

pred show {}

pred showSeriousSystem {
	#User > 1
	#Skill > 1
	#Administrator > 0
	#SuperUser > 0
	#Message > 1
	#Feedback > 1
}
